Nuprl Lemma : comb_for_reduce2_wf
4,23
postcript
pdf
(
A
,
T
,
L
,
k
,
i
,
f
,
z
. reduce2(
f
;
k
;
i
;
L
))
A
,
T
:Type
L
:(
T
List)
A
(
i
:
(
T
{
i
..(
i
+||
L
||)
}
A
A
)
True
A
)
latex
Definitions
,
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
True
,
T
Lemmas
reduce2
wf
,
squash
wf
,
true
wf
,
int
seg
wf
,
length
wf1
,
nat
wf
origin
A,T,L,k,i,f,z. reduce2(f;k;i;L))
A,T:Type
L:(T List)A(i:
(T{i..(i+||L||)
}AA)
TrueA) A,T,L,k,i,f,z. reduce2(f;k;i;L))
A,T:TypeL:(T List)A(i:(T{i..(i+||L||)}AA)TrueA) T
x:A. B(x)}T